Nuprl Lemma : K-implements_wf
11,40
postcript
pdf
Pgm
,
Sem
:Type,
equiv
:(
Sem
Sem
),
S
:(
Pgm
Sem
),
pr
:
Pgm
,
kpr
:(
Sem
Pgm
).
pr
implements
kpr
latex
Definitions
pr
implements
kpr
,
t
T
,
,
x
:
A
.
B
(
x
)
Lemmas
K-sem
wf
origin
Pgm, Sem:Type, equiv:(Sem
Sem
), S:(PgmSem), pr:Pgm, kpr:(SemPgm).
Pgm, Sem:Type, equiv:(SemSem), S:(PgmSem), pr:Pgm, kpr:(SemPgm).
Tx:A. B(x)